/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;

import simhya.matheval.SymbolArray;

/**
 *
 * @author Luca
 */
public class MTLweakUntil  extends MTLmodalNode {
    
    public MTLweakUntil(MTLnode left, MTLnode right) {
        super(new ParametricInterval());
        super.setChildren(left,right);
        left.setParent(this);
        right.setParent(this);
    }

    public MTLweakUntil(ParametricInterval interval, MTLnode left, MTLnode right) {
        super(interval);
        super.setChildren(left,right);
        left.setParent(this);
        right.setParent(this);
    }
    
    @Override
    public String toFormulaTree(int depth) {
        String s = "";
        for (int i=0;i<depth;i++)
            s += "   ";
        s += "Weak Until " + parametricInterval.toString() + "\n";
        return s + super.toFormulaTree(depth);
    }
    
    @Override
    boolean checkGoal(int j) {
        if (j < this.traceLength) 
            return right.truthValue[j];
        else return false;
    }

    @Override
    boolean checkSafe(int j) {
        if (j < this.traceLength) 
            return left.truthValue[j];
        else return false;
    }

    @Override
    void setBad(int i) {
        this.truthValue[i] = false;
    }

    @Override
    void setOk(int i) {
        this.truthValue[i] = true;
    }
    
        @Override
    void labelingFormulaPointwiseSemantics(double [] deltaTimes) {
        /*
         * In order to verify a modal node, different from next,
         * we need to verify if the formula holds in each state of the trace.
         * To do this, we need to find a path from i to j, such that from i to j-1,
         * states are safe; sate j is a goal state, and the time to go from i to j
         * satisfies the metric constrant of the model operator.
         * 
         * We do this backward on the trace, starting from the final state and then going down.
         * We let both i and j point at this final state, then we find the first state from the right 
         * that satisfies the metric bound (can be the last one).
         * 
         * The correctness of the following algorithm can be proved by showing the following invariant
         * that holds at each cycle iteration at point (*)
         * i >= 0 and there is a path of safe states from i to j excluded, and deltaT(i,j) in I
         * and all states from i+1 to n have been assigned the correct truth value.
         * 
         * The invariant is proved by induction, observing that the two while cicles assign the correct 
         * truth value. The second one because the invariant guarantees that all i marked ok are indeed so
         * and the first one set i correctly to bad because t is below the lower bound of the interval 
         * (this holds due to the last while loop) and i cannot reach a goal state in the right time
         * interval (we would have not reached this point with this pair of i-j)
         * When i is an unsafe state, then the formula is false in i, and no state can reach a goal state passing
         * through i, so we can safely move j over i.
         */
        int i = traceLength-1; 
        int j = traceLength-1; 
        double DT = 0; 
        //DT is originally 0, as the last state is the final state ans has duration 0
        double DsafeT = 0;
        double [] safeT = new double[traceLength];
        //DsafeT stores the longest safe path from i, which can go beyond j. 
        while (i >= 0) {
            //here the next action depends on the relative position of DT w.r.t. the metric interval I
            RelativePosition pos = metricInterval.relativePositionOf(DT);
            if (pos == RelativePosition.ON_THE_LEFT) {
                //in this case, there is a good path from i to j (unless j<i),
                //but DT does not satisfy the metric constraint because it is two small. 
                //Hence, i is bad, as no state after j can make it a good state)
                setBad(i); //signals i as a bad state
                safeT[i] = DsafeT;
                i--;
                if (i >= 0) {
                    if (!checkSafe(i)) {
                        //if the new i state is not safe, then no path can pass through it, 
                        //hence we can move j over i
                        DT = updateDT(DT, i+1, i, j, i, deltaTimes);
                        j = i;
                        DsafeT = (i>0 ? -deltaTimes[i-1] : 0);
                    } else {//if i is safe, we just update DT
                        DT = updateDT(DT, i+1, i, j, j, deltaTimes);
                        DsafeT += deltaTimes[i];
                    }
                }
            } else if (pos == RelativePosition.ON_THE_RIGHT) {
                //here the metric bound is not fulfilled because DT is on the right
                //of I, hence j is too distant from i, and we need to move j left
                j--;
                DT = updateDT(DT, i, i, j+1, j, deltaTimes);
            } else if (pos == RelativePosition.OVERLAPS) {
                if (checkGoal(j)) { 
                    setOk(i);
                    safeT[i] = DsafeT;
                    i--;
                    if (i >= 0) {
                        if (!checkSafe(i)) {
                            //if the new i state is not safe, then no path can pass through it, 
                            //hence we can move j over i
                            DT = updateDT(DT, i+1, i, j, i, deltaTimes);
                            j = i;
                            DsafeT = (i>0 ? -deltaTimes[i-1] : 0);
                        } else {//if i is safe, we just update DT
                            DT = updateDT(DT, i+1, i, j, j, deltaTimes);
                            DsafeT += deltaTimes[i];
                        }
                    }
                } else {
                    //if j is not a goal state, then we can move it on the left
                    j--;
                    DT = updateDT(DT, i, i, j+1, j, deltaTimes);
                }
            }
        }
        //this should correct for weak semantics of until, by setting as good
        //all those paths from which there is a safe path longer than the metric bound. 
        //notice that infinite weak until always fails in this semantics, that terminates at a finite time. 
        for (int k=0;k<traceLength;k++)
            this.truthValue[k] = this.truthValue[k] || safeT[k] >= metricInterval.upper;
    }
    
    @Override
    void labelingTopFormulaPointwiseSemantics(double [] deltaTimes, 
            boolean varyInterval, boolean varyRightBound, int points) {
        if (varyInterval && !metricInterval.upperIsInfinity &&
                metricInterval.lower < metricInterval.upper && points > 1) {
            //compute the span points
            double delta = (metricInterval.upper - metricInterval.lower)/(points-1);
            double [] span = new double[points];
                for (int i=0;i<points;i++)
                    span[i] = metricInterval.lower + i*delta;
            Interval interval = new Interval();
            if (varyRightBound) {
                interval.setLower(metricInterval.lower, metricInterval.lowerClosed);
                int j = 0;
                double t = 0; //time at state j in trace
                for (int k=0;k<points;k++) {
                    interval.setUpper(span[k], metricInterval.upperClosed);
                    while (true) {
                        if (interval.contains(t) && checkGoal(j)) {
                            //if we enter the metric bound and we find a goal state, then 
                            //we set all remaining points to true
                            for ( ;k<points;k++)
                                setOk(k);
                            break;
                        } else if (interval.upperBoundSmallerThan(t)) {
                            //we have not found a goal state and we overcome the interval
                            //so k is good, according to the weak semantics of until
                            setOk(k); 
                            break;
                        } 
                        //if we are here, we need to check if the system is safe
                        if (checkSafe(j)) {
                            //if we find not a goal but a safe state, we advance to next state
                            t += deltaTimes[j];
                            j++;
                        } else {
                            //if we enter an unsafe state then we set all states as bad
                             for ( ;k<points;k++)
                                setBad(k);
                             break;
                        }
                    }
                }
            } else {
                interval.setUpper(metricInterval.upper, metricInterval.upperClosed);
                int j = 0;
                double t = 0; //time at state j in trace
                for (int k=0;k<points;k++) {
                    interval.setLower(span[k], metricInterval.lowerClosed);
                    while (true) {
                        if (interval.contains(t) && checkGoal(j)) {
                            //if we enter the metric bound and we find a goal state, then 
                            //we set the current k to ok and we continue.
                            setOk(k);
                            break;
                        } else if (interval.upperBoundSmallerThan(t)) {
                            //we have not found a goal state and we overcome the interval
                            //we can signal as good all states
                            for ( ;k<points;k++)
                                setOk(k);
                             break;
                        } 
                        //if we are here, we need to check if the system is safe
                        if (checkSafe(j)) {
                            //if we find not a goal but a safe state, we advance to next state
                            t += deltaTimes[j];
                            j++;
                        } else {
                            //if we enter an unsafe state then we set all states as bad
                             for ( ;k<points;k++)
                                setBad(k);
                             break;
                        }
                    }
                }
            }
        } else {
            //in this case, we just need to aswer yes or no
            int j = 0;
            double t = 0; //time at state j in trace
            while (true) {
                if (metricInterval.contains(t) && checkGoal(j)) {
                    //if we enter the metric bound and we find a goal state, then 
                    //we set all remaining points to true
                    setOk(0);
                    break;
                } else if (metricInterval.upperBoundSmallerThan(t)) {
                    //we have not found a goal state and we overcome the interval
                    //so the trace is bad
                    setOk(0); 
                    break;
                } 
                //if we are here, we need to check if the system is safe
                if (checkSafe(j)) {
                    //if we find not a goal but a safe state, we advance to next state
                    t += deltaTimes[j];
                    j++;
                } else {
                    //if we enter an unsafe state then we set the trace as bad
                     setBad(0);
                     break;
                }
            }
        }
    }
    
    

}
